% !Mode:: "TeX:UTF-8"
@MANUAL{mips64II,
  TITLE =        {MIPS64™ Architecture For Programmers. Volume II: The MIPS64™ Instruction Set},
  organization = {MIPS Technologies},
  year =         {2001},
}

@MANUAL{mips64III,
  TITLE =        {MIPS64™ Architecture For Programmers. Volume III: The MIPS64™ Privileged Resource Architecture},
  organization = {MIPS Technologies},
  year =         {2001},
}

@BOOK{mips64DONTUSE,
  TITLE =        {MIPS64™ Architecture For Programmers},
  PUBLISHER =    {MIPS Technologies, Inc.},
  YEAR =         {2003},
}

@ARTICLE{AckermannDONTUSE,
  AUTHOR =       {W. Ackermann},
  TITLE =        {Solvable cases of the Decision Problem},
  JOURNAL =      {Studies in Logic and the Foundations of Mathematics},
  YEAR =         {1954},
}

@ARTICLE{GenesysPro,
  AUTHOR =       {A. Adir and E. Almog and L. Fournier and
  E. Marcus and M. Rimon and M. Vinov and A. Ziv},
  TITLE =        {Industrial Experience with Test Generation Languages for Processor Verification},
  JOURNAL =      {IEEE Design and Test of Computers},
  YEAR =         {2004},
  volume =       {21},
  number =       {2},
  pages =        {84-93},
  month =        {Mar./Apr.},
}

@ARTICLE{GenesysPro2004Innovations,
  AUTHOR =       {A. Adir and E. Almog and L. Fournier and E. Marcus and M. Rimon and M. Vinov and A. Ziv},
  TITLE =        {Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification},
  JOURNAL =      {IEEE Design and Test of Computers},
  YEAR =         {2004},
  volume =       {21},
  number =       {2},
  pages =        {84-93},
  month =        {Mar/Apr},
}

@article{GenesysSolver,
  author    = {E. Bin and R. Emek and G. Shurek and A. Ziv},
  title     = {Using a constraint satisfaction formulation and solution
               techniques for random test program generation},
  journal   = {IBM Systems Journal},
  volume    = {41},
  number    = {3},
  year      = {2002},
  pages     = {386-402},
  ee        = {http://researchweb.watson.ibm.com/journal/sj/413/bin.html},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DeepTrans,
  author    = {A. Adir and R. Emek and Y. Katz and A. Koyfman},
  title     = {DeepTrans --- A Model-based Approach to Functional Verification
               of Address Translation Mechanisms},
  booktitle = {MTV},
  year      = {2003},
  pages     = {3-6},
  ee        = {http://csdl.computer.org/comp/proceedings/mtv/2003/2045/00/20450003abs.htm},
  journal   = {Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions},
}


@book{CSP,
 author = {F. Rossi and van Beek, P. and T. Walsh},
 title = {Handbook of Constraint Programming (Foundations of Artificial Intelligence)},
 year = {2006},
 isbn = {0444527265},
 publisher = {Elsevier Science Inc.},
 address = {New York, NY, USA},
}

@book{CLPusingECLiPSe,
 author = {Apt, K. R. and M. Wallace},
 title = {Constraint Logic Programming using Eclipse},
 year = {2007},
 isbn = {0521866286},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@MANUAL{SICStus,
  TITLE =        {SICStus Prolog User’s manual, release 4},
  organization = {Intelligent Systems Laboratory, Swedish Institute of Computer Science},
  year =         {2009},
}

@ARTICLE{ILOG,
  AUTHOR =       {Puget, J.-F.},
  TITLE =        {A C++ implementation of CLP},
  JOURNAL =      {Proceedings of the 2nd Singapore International Conference on Intelligent Systems},
  YEAR =         {1994},
}

@BOOK{FundamentalOfComputerOrganizationAndDesign,
  AUTHOR =       {Dandamudi, S. P.},
  TITLE =        {Fundamentals of computer organization and design},
  PUBLISHER =    {Springer},
  YEAR =         {2003},
}

@ARTICLE{MicroTESK,
  AUTHOR =       {Камкин, А. С.},
  TITLE =        {Комбинаторная генерация тестовых программ для микропроцессоров на основе моделей},
  JOURNAL =      {Препринт Института Системного Программирования РАН},
  YEAR =         {2008},
  volume =       {21},
  language =     {russian},
}

@ARTICLE{muGPDONTUSE,
  AUTHOR =       {F. Corno and E. Sanchez and M. S. Reorda and G. Squillero},
  TITLE =        {Automatic Test Program Generation -- a Case Study},
  JOURNAL =      {IEEE Design \& Test, Special issue on Functional Verification and Testbench Generation},
  YEAR =         {2001},
  volume =       {21},
  number =       {2},
  pages =        {102-109},
  month =        {March-April},
}


@ARTICLE{TSE,
  AUTHOR =       {F. Fallah and K. Takayama},
  TITLE =        {A New Functional Test Program Generation Methodology},
  JOURNAL =      {Proceedings 2001 IEEE International Conference on Computer Design: VLSI in Computers and Processors},
  YEAR =         {2001},
  pages =        {76-81},
}

@ARTICLE{mVpGen,
  AUTHOR =       {K. Kohno and N. Matsumoto},
  TITLE =        {A New Verification Methodology for Complex Pipeline Behavior},
  JOURNAL =      {Proceedings of the 38st Design Automation Conference (DAC’01)},
  YEAR =         {2001},
}

@ARTICLE{ISDL,
  AUTHOR =       {G. Hadjiyiannis and S. Hanono and S. Devadas},
  TITLE =        {ISDL: An Instruction Set Description Language for Retargetability},
  JOURNAL =      {Proceedings of the 34th Design Auiomation Conference},
  YEAR =         {1997},
  pages =        {299-302},
  month =        {June},
}

@ARTICLE{toATPG,
  AUTHOR =       {M. Beardo and F. Bruschi and F. Ferrandi and D. Sciuto},
  TITLE =        {An Approach to Functional Testing of VLIW Architectures},
  JOURNAL =      {Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT'00)},
  YEAR =         {2000},
  pages =        {29-33},
}

@book{ATPGbook,
 author = {A. Miczo},
 title = {Digital logic testing and simulation},
 year = {2003},
 publisher = {Wiley-Interscience; 2 edition},
}

@BOOK{VHDL,
  AUTHOR =       {P. J. Ashenden},
  TITLE =        {The Designer's Guide to VHDL},
  PUBLISHER =    {Elsevier},
  YEAR =         {2008},
}

@ARTICLE{MAATG,
  AUTHOR =       {T. Li and D. Zhu and Y. Guo and G. Liu and S. Li},
  TITLE =        {MAATG: A Functional Test Program Generator for Microprocessor Verification},
  JOURNAL =      {Proceedings of the 2005 8th Euromicro conference on Digital System Design (DSD’05)},
  YEAR =         {2005},
}

@INPROCEEDINGS{expression,
    author = {A. Halambi and P. Grun and V. Ganesh and A. Khare and N. Dutt and A. Nicolau},
    title = {EXPRESSION: A Language for Architecture Exploration through Compiler/Simulator Retargetability.},
    booktitle = {Proceedings of the European Conference on Design, Automation and Test},
    year = {1999},
    pages = {485--490}
}


@BOOK{HennesyPatterson,
  AUTHOR =       {J. L. Hennessy and D. A. Patterson and A. C. Arpaci-Dusseau},
  TITLE =        {Computer architecture: a quantitative approach},
  PUBLISHER =    {Morgan Kaufmann},
  YEAR =         {2007},
  edition =      {4},
}

@BOOK{HennessyPatterson3rd,
  AUTHOR =       {J. L. Hennessy and D. A. Patterson},
  TITLE =        {Computer architecture: a quantitative approach},
  PUBLISHER =    {Morgan Kaufmann},
  YEAR =         {2003},
  edition =      {3},
}

@inproceedings{GenesysTK,
  author    = {L. Fournier and Y. Arbetman and M. Levinger},
  title     = {Functional Verification Methodology for Microprocessors
               Using the Genesys Test-Program Generator-Application to
               the x86 Microprocessors Family},
  booktitle = {DATE},
  year      = {1999},
  pages     = {434-441},
  ee        = {http://csdl.computer.org/comp/proceedings/date/1999/0078/00/00780434abs.htm},
  crossref  = {DBLP:conf/date/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{shnitman,
  AUTHOR =       {Шнитман, В. З.},
  TITLE =        {Современные высокопроизводительные компьютеры},
  JOURNAL =      {Центр информационных технологий},
  YEAR =         {1996},
  language =     {russian},
}

@TECHREPORT{PowerPC750,
  TITLE =        {PowerPC 750 RISC Microprocessor Technical Summary},
  INSTITUTION =  {Motorola},
  YEAR =         {1997},
}

@TECHREPORT{PowerPC970FXUserManual,
  TITLE =        {PowerPC G5 User's Manual},
  INSTITUTION =  {IBM},
  YEAR =         {2008},
}

@ARTICLE{Z3,
  AUTHOR =       {de Moura, L. and N. Bj{\o}rner},
  TITLE =        {Z3: An Efficient SMT Solver},
  JOURNAL =      {Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  YEAR =         {2008},
}

@ARTICLE{Yices,
  AUTHOR =       {de Moura, L. and B. Dutertre},
  TITLE =        {Yices 1.0: An Efficient SMT solver},
  JOURNAL =      {The Satisfiability Modulo Theories Competition (SMT--COMP)},
  YEAR =         {2006},
}

@ARTICLE{my_syrcose_2008,
  AUTHOR =       {E. Kornikhin},
  TITLE =        {Test Data Generation for Arithmetic Subsystem of CPUs MIPS64},
  JOURNAL =      {Proceedings of Spring Young Researchers Colloqium on Software Engineering},
  YEAR =         {2008},
  volume =       {2},
  pages =        {43--46},
}

@ARTICLE{my_isp_2008,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Генерация тестовых данных для тестирования арифметических операций центральных процессоров},
  JOURNAL =      {Труды Института Системного Программирования},
  YEAR =         {2008},
  volume =       {15},
  pages =        {107-117},
  language =     {russian},
}

@ARTICLE{my_lomonosov_2009,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Система генерации тестовых программ с использованием ограничений ТЕСЛА},
  JOURNAL =      {Сборник тезисов конференции Ломоносов},
  YEAR =         {2009},
  pages =        {39},
  language =     {russian},
}

@ARTICLE{my_lomonosov_2010,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Определение стратегии вытеснения PseudoLRU на ветвях бинарного дерева},
  JOURNAL =      {Сборник тезисов конференции Ломоносов},
  YEAR =         {2010},
  pages =        {20--21},
  language =     {russian},
}

@ARTICLE{my_miet_2009,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА},
  JOURNAL =      {Сборник тезисов конференции <<Микроэлектроника и информатика>>},
  YEAR =         {2009},
  pages =        {87},
  language =     {russian},
}

@ARTICLE{my_nivc_2009,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Генерация тестовых данных для системного функционального тестирования FIFO-кэш-памяти микропроцессоров},
  JOURNAL =      {Вычислительные методы и программирование},
  YEAR =         {2009},
  volume =       {10},
  pages =        {107--116},
  language =     {russian},
}

@ARTICLE{my_syrcose_2009,
  AUTHOR =       {E. Kornikhin},
  TITLE =        {Test Data Generation for LRU Cache-Memory testing},
  JOURNAL =      {Proceedings of Spring Young Researchers Colloqium on Software Engineering},
  YEAR =         {2009},
  pages =        {88--92},
}

@ARTICLE{my_isp_2009,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Генерация тестовых данных для системного
  функционального тестирования микропроцессоров с учетом кэширования
  и трансляции адресов},
  JOURNAL =      {Труды Института Системного Программирования},
  YEAR =         {2009},
  volume =       {17},
  pages =        {145--160},
  language =     {russian},
}

@ARTICLE{my_isp_2010UNDEFINED,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Метод зеркальной генерации ограничений для построения тестовых программ по тестовым шаблонам},
  JOURNAL =      {Труды Института Системного Программирования},
  YEAR =         {2010},
  volume =       {??},
  pages =        {??},
  language =     {russian},
}

@ARTICLE{my_ewdts_2009,
  AUTHOR =       {E. Kornikhin},
  TITLE =        {SMT-based Test Program Generation for Cache-memory Testing},
  JOURNAL =      {Proceedings of East-West D T S},
  YEAR =         {2009},
  pages =        {124--127},
}

@ARTICLE{my_programmirovanie_2010,
  AUTHOR =       {Корныхин, Е. В.},
  TITLE =        {Генерация тестовых данных для тестирования механизмов кэширования и трансляции адресов микропроцессоров},
  JOURNAL =      {Программирование},
  YEAR =         {2010},
  volume =       {36},
  number =       {1},
  pages =        {40--49},
  language =     {russian},
}

@BOOK{my_preprint,
  AUTHOR =       {Камкин, А.С. and Корныхин, Е. В.},
  TITLE =        {Построение тестовых программ для верификации подсистем управления памятью микропроцессоров},
  address =      {М.},
  note =         {Препринт Института системного программирования РАН},
  YEAR =         {2010},
%  volume =       {??},
%  pages =        {??},
  language =     {russian},
}

@article{policy_tables,
  author    = {D. Grund and J. Reineke},
  title     = {Estimating the Performance of Cache Replacement Policies},
  year      = {2008},
  pages     = {101-112},
  ee        = {http://dx.doi.org/10.1109/MEMCOD.2008.4547695},
  journal   = {6th ACM {\&} IEEE International Conference on Formal Methods
               and Models for Co-Design (MEMOCODE 2008), June 5-7, 2008,
               Anaheim, CA, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn      = {978-1-4244-2417-7},
  publisher = {IEEE Computer Society},
}

% +
@ARTICLE{vorobyev,
  AUTHOR =       {Воробьев, Д. Н. and Камкин, А. С.},
  TITLE =        {Генерация тестовых программ для подсистемы управления памятью микропроцессоров},
  JOURNAL =      {Труды Института Системного Программирования РАН},
  YEAR =         {2009},
  language =     {russian},
  volume   =     {17},
  pages =        {119--132},
  address =      {М.},
  publisher =    {РАН},
}

% +
@ARTICLE{thompson,
  AUTHOR =       {Б. Томпсон},
  TITLE =        {Управление памятью},
  JOURNAL =      {Computerworld Россия},
  YEAR =         {2001},
  language =     {russian},
  number =       {22},
}

% +
@BOOK{Pasko,
  AUTHOR =       {В. П. Пасько},
  TITLE =        {Энциклопедия ПК. Аппаратура.Программы.Интернет},
  ADDRESS =      {СПб.},
  PUBLISHER =    {Питер},
  YEAR =         {2004},
  language =     {russian},
  pages =        {800},
}

@ARTICLE{montanari,
  AUTHOR =       {U. Montanari},
  TITLE =        {Networks of constraints: Fundamental properties and applications to picture processing},
  JOURNAL =      {Information Sciences},
  YEAR =         {1974},
  volume =       {7},
  pages =        {95-132},
}

@ARTICLE{CSPS1,
  AUTHOR =       {R. Bartak},
  TITLE =        {Theory and practice of constraint propagation},
  JOURNAL =      {Proceedings of the Third Workshop
on Constraint Programming for Decision and Control (CPDC-01)},
  YEAR =         {2001},
  pages =        {7--14},
}

@TECHREPORT{CSPS2,
  AUTHOR =       {R. Dechter and D. Frost},
  TITLE =        {Backtracking algorithms for constraint satisfaction problems},
  INSTITUTION =  {Department of Information and Computer Science, University of California, Irvine},
  YEAR =         {1999},
}

@ARTICLE{CSPS3,
  AUTHOR =       {V. Kumar},
  TITLE =        {Algorithms for constraint satisfaction problems: A survey},
  JOURNAL =      {AI Magazine},
  YEAR =         {1992},
  volume =       {13},
  number =       {1},
  pages =        {32--44},
}

@book{DPLL,
  editor    = {J. A. Robinson and A. Voronkov},
  title     = {Handbook of Automated Reasoning (in 2 volumes)},
  publisher = {Elsevier and MIT Press},
  year      = {2001},
  isbn      = {0-444-50813-9, 0-262-18223-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{DPLL60,
  AUTHOR =       {M. Davis and H. Putnam},
  TITLE =        {A computing procedure for quantification theory},
  JOURNAL =      {Journal of the Association for Computing Machinery},
  YEAR =         {1960},
  volume =       {7},
  number =       {3},
  pages =        {201--215},
}

@ARTICLE{DPLL62,
  AUTHOR =       {M. Davis and G. Logemann and D. Loveland},
  TITLE =        {A machine program for theorem-proving},
  JOURNAL =      {Communications of the Association for Computing Machinery},
  YEAR =         {1962},
  volume =       {5},
  pages =        {394--397},
}

@ARTICLE{Chaff,
  AUTHOR =       {M. Moskewicz and C. Madigan and Y. Zhao and L. Zhang and S. Malik},
  TITLE =        {Chaff: Engineering an Efficient SAT Solver},
  JOURNAL =      {Proceedings of the 39th Design Automation
Conference (DAC 2001), Las Vegas},
  YEAR =         {2001},
}

@ARTICLE{WalkSAT,
  AUTHOR =       {B. Selman and H. Kautz and B. Cohen},
  TITLE =        {Local Search Strategies for Satisfiability Testing},
  JOURNAL =      {Cliques, Coloring, and Satisfiability: Second DIMACS Implementation
Challenge},
  YEAR =         {1993},
}

@BOOK{DecisionProcedures,
  AUTHOR =       {D. Kroening and O. Strichman},
  TITLE =        {Decision Procedures: an algorithmic point of view},
  PUBLISHER =    {Springer},
  YEAR =         {2008},
  isbn =         {978-3540741046},
}

@ARTICLE{OppenNelsonPresburger,
  AUTHOR =       {G. Nelson and D. C. Oppen},
  TITLE =        {A simplifier based on efficient decision algorithms},
  JOURNAL =      {Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages},
  YEAR =         {1978},
  pages =        {141–-150},
}

@ARTICLE{Tveretina,
  AUTHOR =       {O. Tveretina},
  TITLE =        {A decision procedure for equality logic with uninterpreted functions},
  JOURNAL =      {Artificial Intelligence and Symbolic Mathematical Computation,
Lecture Notes in Artificial Intelligence},
  YEAR =         {2004},
  volume =       {3249},
  pages =        {63--76},
}

@article{ DecisionRealPolynomials,
author = {L. Adleman and K. Manders},
title = {Computational complexity of decision procedures for polynomials},
journal ={Symposium on Foundations of Computer Science},
volume = {0},
year = {1975},
issn = {0272-5428},
pages = {169-177},
doi = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1975.9},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}

@ARTICLE{NelsonOppenProcedure,
  AUTHOR =       {G. Nelson and D. C. Oppen},
  TITLE =        {Simplification by Cooperating Decision Procedures},
  JOURNAL =      {ACM Transactions on Programming Languages and Systems},
  YEAR =         {1979},
  volume =       {1},
  number =       {2},
  pages =        {245--257},
}

@ARTICLE{Shostak,
  AUTHOR =       {R. E. Shostak},
  TITLE =        {Deciding Combinations of Theories},
  JOURNAL =      {Journal of the ACM},
  YEAR =         {1984},
  volume =       {31},
  pages =        {1--12},
}


@ARTICLE{DTC,
  AUTHOR =       {M. Bozzano and R. Bruttomesso and A. Cimatti and
  T. Junttila and van Rossum, P. and S. Ranise and R. Sebastiani},
  TITLE =        {Efficient Satisfiability Modulo Theories via Delayed Theory Combination},
  JOURNAL =      {Proceedings of the International Conference on Computer-Aided Verification, CAV 2005},
  YEAR =         {2005},
}

@ARTICLE{MathSAT_RTL,
  AUTHOR =       {M. Bozzano and R. Bruttomesso and A. Cimatti and A.
  Franzen and Z. Hanna and Z. Khasidashvili and A. Palti and R. Sebastiani},
  TITLE =        {Encoding RTL Constructs for MathSAT: a Preliminary Report},
  JOURNAL =      {Proceedings of the PDPAR'05},
  YEAR =         {2006},
}

@ARTICLE{SMT_Pipeline,
  AUTHOR =       {J. R. Burch and D. L. Dill},
  TITLE =        {Automatic Verification of Pipelined Microprocessor Control},
  JOURNAL =      {Proceedings of CAV '94},
  YEAR =         {1994},
}

@ARTICLE{SMT_Circuets,
  AUTHOR =       {G. Parthasarathy and M. K. Iyer and Cheng, K.-T. and Wang, L.­C. },
  TITLE =        {An efficient finite~-~domain constraint solver for circuits},
  JOURNAL =      {Proceedings of DAC'04},
  YEAR =         {2004},
}

@ARTICLE{Bryant,
  AUTHOR =       {E. Bryant and S. M. German and M. N. Velev},
  TITLE =        {Microprocessor
Verification Using Efficient Decision Procedures for a Logic of
Equality with Uninterpreted Functions},
  JOURNAL =      {Analytic Tableaux and Related Methods},
  YEAR =         {1999},
  pages =        {1--13},
}

@article{ smt_debugging,
author = {A. S\"{u}lflow and R. Wille and G. Fey and R. Drechsler},
title = {Evaluation of Cardinality Constraints on SMT-Based Debugging},
journal ={Multiple-Valued Logic, IEEE International Symposium on},
volume = {0},
year = {2009},
issn = {0195-623X},
pages = {298-303},
doi = {http://doi.ieeecomputersociety.org/10.1109/ISMVL.2009.28},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}

@article{PiskacK08,
  author    = {R. Piskac and V. Kuncak},
  title     = {Decision Procedures for Multisets with Cardinality Constraints},
  year      = {2008},
  pages     = {218-232},
  journal     = {Proceedings of the 9th International Conference on
                Verification, Model Checking, and Abstract Interpretation,
               VMCAI 2008, San Francisco,
               USA},
}

@article{KuncakR07,
  author    = {V. Kuncak and M. C. Rinard},
  title     = {Towards Efficient Satisfiability Checking for Boolean Algebra
               with Presburger Arithmetic},
  booktitle = {CADE},
  year      = {2007},
  pages     = {215-230},
  journal     = {Proceedings of the 21st International Conference
               on Automated Deduction CADE, Bremen, Germany, July 17-20},
}


@article{Revesz05,
  author    = {P. Z. Revesz},
  title     = {The Expressivity of Constraint Query Languages with Boolean
               Algebra Linear Cardinality Constraints},
  journal     = {Proceedings of Advances in Databases and Information Systems, 9th East
               European Conference, ADBIS 2005, Tallinn, Estonia, September
               12-15, 2005, Proceedings},
  booktitle = {ADBIS},
  year      = {2005},
  pages     = {167-182},
}

@ARTICLE{DART,
  AUTHOR =       {C. Pacheco and S. K. Lahiri and M. D. Ernst and T. Ball},
  TITLE =        {Feedback-Directed Random Test Generation},
  JOURNAL =      {Proceedings of the 29th International Conference on Software Engineering},
  YEAR =         {2007},
  pages =        {75--84},
}

@ARTICLE{MonteKarlo,
  AUTHOR =       {N. Metropolis and S. Ulam},
  TITLE =        {The Monte Carlo Method},
  JOURNAL =      {Journal of American Statistical Association},
  YEAR =         {1949},
  volume =       {44},
  number =       {247},
  pages =        {335--341},
}

@BOOK{MMU,
  AUTHOR =       {S. G. Shiva},
  TITLE =        {Computer design and architecture},
  PUBLISHER =    {Atlantic/Little, Brown},
  YEAR =         {2000},
  edition =      {3d},
}

@ARTICLE{Kuliamin_verification,
  AUTHOR =       {Кулямин, В. В.},
  TITLE =        {Интеграция методов верификации программного обеспечения},
  JOURNAL =      {Программирование},
  YEAR =         {2009},
  volume =       {35},
  number =       {4},
  pages =        {212--222},
  language =     {russian},
}

@BOOK{Kuliamin_course,
  AUTHOR =       {Кулямин, В. В.},
  TITLE =        {Технологии программирования. Компонентный подход},
  PUBLISHER =    {ИНТУИТ-Бином},
  YEAR =         {2007},
  address =      {М.},
  pages =        {463},
  language =     {russian},
}

@ARTICLE{UniTESK,
  AUTHOR =       {Баранцев, А. В. and Бурдонов, И. Б. and Демаков, А. В. and Зеленов, С. В.
  and Косачев, А. С. and Кулямин, В. В. and Омельченко, В. А. and Пакулин, Н. В. and
  Петренко, А. К. and Хорошилов, А. В.},
  TITLE =        {Подход UniTESK к разработке тестов: достижения и перспективы},
  JOURNAL =      {Труды Института Системного Программирования РАН},
  YEAR =         {2004},
  volume =       {5},
  pages =        {121--156},
  language =     {russian},
}

@ARTICLE{Alpha21364,
  AUTHOR =       {L. Gwennap},
  TITLE =        {Alpha 21364 to ease memory bottleneck},
  JOURNAL =      {Microprocessor Report},
  YEAR =         {1998},
  volume =       {12},
  number =       {14},
  pages =        {12--15},
}

@ARTICLE{Cell,
  AUTHOR =       {Д. Кэйхел and М. Дэй and П. Хофсти and Ч. Джонс and Т. Маерер and Д. Шиппи},
  TITLE =        {Мультипроцессор Cell},
  JOURNAL =      {Открытые системы},
  YEAR =         {2006},
  number =       {5},
}

@ARTICLE{Alpha21264,
  AUTHOR =       {Kessler, R. E.},
  TITLE =        {The Alpha 21264 Microprocessor},
  JOURNAL =      {IEEE Micro},
  YEAR =         {1999},
  volume =       {19},
  number =       {2},
  pages =        {24--36},
}

@UNPUBLISHED{RAVEN,
  AUTHOR =       {E. Hennenhoefer and M. Typaldos},
  TITLE =        {The Evolution of Processor Test Generation Technology},
  NOTE =         {Obsidian Software Inc.},
  year =         {2008},
}

@ARTICLE{isaac05balanced,
  AUTHOR =       {C. Bazgan and M. Karpinski},
  TITLE =        {On the Complexity of Global Constraint Satisfaction},
  JOURNAL =      {LNCS 3827},
  YEAR =         {2005},
  pages =        {624--633},
}

@article{Berkeley89,
	author = 	{D. A. Wood and G. A. Gibson and R. H. Katz},
	title = 	{Verifying a Multiprocessor Cache Controller Using Random Test Generation},
	journal =	{IEEE Design and Test of Computers},
	volume = 	{7},
	issn = 		{0740-7475},
	year = 		{1990},
	pages = 	{13-25},
	doi = {http://doi.ieeecomputersociety.org/10.1109/54.57906},
	publisher = {IEEE Computer Society},
	address = {Los Alamitos, CA, USA},
}

@BOOK{ModelChecking,
  AUTHOR = {E. M. Clarke and O. Grumberg and D. A. Peled},
  TITLE = {Model Checking},
  PUBLISHER = {MIT Press},
  ADDRESS = {Cambridge, MA},
  YEAR = {1999},
}

@article{MishraDutt02,
	author = {P. Mishra and N. Dutt},
	title = {Automatic functional test program generation for pipelined processors using model checking},
	journal = {High-Level Design, Validation, and Test Workshop, IEEE International},
	volume = {0},
	isbn = {0-7803-7655-2},
	year = {2002},
	pages = {99-103},
	doi = {http://doi.ieeecomputersociety.org/10.1109/HLDVT.2002.1224436},
	publisher = {IEEE Computer Society},
	address = {Los Alamitos, CA, USA},
}

@INPROCEEDINGS{MishraDutt04,
    author = {P. Mishra and N. Dutt},
    title = {Graph-based functional test program generation for pipelined processors},
    booktitle = {In Proceedings of Design Automation and Test in Europe (DATE},
    year = {2004},
    pages = {182--187}
}

@article{MishraDutt05,
 author = {Mishra, P. and Dutt, N.},
 title = {Functional Coverage Driven Test Generation for Validation of Pipelined Processors},
 booktitle = {DATE '05: Proceedings of the conference on Design, Automation and Test in Europe},
 year = {2005},
 isbn = {0-7695-2288-2},
 pages = {678--683},
 doi = {http://dx.doi.org/10.1109/DATE.2005.162},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

@article{Mishra09,
  author    = {Koo, H.-M. and P. Mishra},
  title     = {Functional test generation using design and property decomposition
               techniques},
  journal   = {ACM Transactions on Embedded Computer Systems},
  volume    = {8},
  number    = {4},
  year      = {2009},
  ee        = {http://doi.acm.org/10.1145/1550987.1550995},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{SMV,
	author 		= {K. L. McMillan},
	title			= {Symbolic Model Checking},
	publisher	= {Kluwer Academic Publishers},
	year			= {1993},
}

@inproceedings{microGP,
 author = {Corno, F. and Cumani, G. and Reorda, S. M. and Squillero, G.},
 title = {Fully Automatic Test Program Generation for Microprocessor Cores},
 booktitle = {DATE '03: Proceedings of the conference on Design, Automation and Test in Europe},
 year = {2003},
 isbn = {0-7695-1870-2},
 pages = {11006},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

@inproceedings{Branches99,
 author = {Utamaphethai, N. and Blanton, R. D.  and Shen, J. P.},
 title = {Superscalar Processor Validation at the Microarchitecture Level},
 booktitle = {VLSID '99: Proceedings of the 12th International Conference on VLSI Design - 'VLSI for the Information Appliance'},
 year = {1999},
 isbn = {0-7695-0013-7},
 pages = {300},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

@inproceedings{UrFSM,
 author = {Ur, S. and Yadin, Y.},
 title = {Micro architecture coverage directed generation of test programs},
 booktitle = {DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference},
 year = {1999},
 isbn = {1-58133-109-7},
 pages = {175--180},
 location = {New Orleans, Louisiana, United States},
 doi = {http://doi.acm.org/10.1145/309847.309909},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{R10000,
	author	= {Yeager, K. C.},
	title		= {The Mips R10000 Superscalar Microprocessor},
	year		= {1996},
	journal	= {IEEE Micro},
	volume	= {16},
	number	= {2},
	pages		= {28--40},
}

@inproceedings{SEGUE1,
 author = {Taylor, S. and Quinn, M. and Brown, D. and Dohm, N. and Hildebrandt, S. and Huggins, J. and Ramey, C.},
 title = {Functional verification of a multiple-issue, out-of-order, superscalar Alpha processor---the DEC Alpha 21264 microprocessor},
 booktitle = {DAC '98: Proceedings of the 35th annual Design Automation Conference},
 year = {1998},
 isbn = {0-89791-964-5},
 pages = {638--643},
 location = {San Francisco, California, United States},
 doi = {http://doi.acm.org/10.1145/277044.277208},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{SEGUE2,
 author = {Anderson, W.},
 title = {Logical Verification of the NVAX CPU Chip Design},
 booktitle = {ICCD '92: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer \& Processors},
 year = {1992},
 isbn = {0-8186-3110-4},
 pages = {306--309},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

@article{PA-RISC,
	author 	= {Mangelsdorf, S. T. and Gratias, R. E and Blumberg, R. M. and Bhatia, R.},
	title		= {Functional verification of the HP PA 8000 processor},
	journal	= {Hewlett-Packard Journal},
	pages		= {1--13},
	year		= {1997},
	month		= {август},
}

@inproceedings{Theo,
 author = {Shen, J. and Abraham, J. and Baker, D. and Hurson, T. and Kinkade, M. and Gervasio, G. and Chu, C.-c. and Hu, G.},
 title = {Functional verification of the equator MAP1000 microprocessor},
 booktitle = {DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference},
 year = {1999},
 isbn = {1-58133-109-7},
 pages = {169--174},
 location = {New Orleans, Louisiana, United States},
 doi = {http://doi.acm.org/10.1145/309847.309908},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{GeneticTemplates,
 author = {Corno, F. and Reorda, M. S. and Squillero, S. and Violante, M.},
 title = {On the test of microprocessor IP cores},
 booktitle = {DATE '01: Proceedings of the conference on Design, automation and test in Europe},
 year = {2001},
 isbn = {0-7695-0993-2},
 pages = {209--213},
 location = {Munich, Germany},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 }

@article{SMT,
 author = {de Moura, L. and Bj{\o}rner, N.},
 title = {Satisfiability Modulo Theories: An Appetizer},
 book = {Formal Methods: Foundations and Applications: 12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers},
 year = {2009},
 isbn = {978-3-642-10451-0},
 pages = {23--36},
 doi = {http://dx.doi.org/10.1007/978-3-642-10452-7_3},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 }


@MISC{IntelCacheOLD,
      TITLE = "An Overview of Cache",
      PUBLISHER =    {Intel},
      NOTE = "http://www.intel.com/design/intarch/papers/cache6.htm"
}

@MISC{IntelCache,
      NOTE = "http://www.intel.com/design/intarch/papers/cache6.htm"
}

% +
@book{Kasperski_EffectiveMemory,
	author		= {Касперски, К.},
	title		= {Техника оптимизации программ. Эффективное использование памяти},
    address     = {СПб.},
	publisher	= {БХВ-Петербург},
	year		= {2003},
    pages       = {560},
}

@techreport{MOBs,
	author		= {S. Petters},
	title			= {Intel Architecture Software Developer’s Manual Volume 3: System Programming},
	year			= {2001},
}

@book{VerilogDesign,
	title			= {RTL hardware design using VHDL: coding for efficiency, portability, and scalability},
	author		= {P. P. Chu},
	publisher	= {John Wiley and Sons},
	year			= {2006},
	isbn			= {9780471720928},
	pages			=	{669},
}

@article{UnitCoreLevel,
author = {K. Murale and S. Hildebrandt and P. Bojsen and A. Urzua},
title = {AMD64 Processor Front-End Verification (at Unit-Level Testbench) with Instruction Set Simulator},
journal ={Microprocessor Test and Verification, International Workshop on},
volume = {0},
issn = {1550-4093},
year = {2008},
pages = {81-87},
doi = {http://doi.ieeecomputersociety.org/10.1109/MTV.2008.12},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}

@book{SimulationBased,
 author = {Lam, W. K.},
 title = {Hardware Design Verification: Simulation and Formal Method-Based Approaches},
 year = {2008},
 isbn = {0137010923, 9780137010929},
 publisher = {Prentice Hall PTR},
 address = {Upper Saddle River, NJ, USA},
	pages = {624},
}

@techreport{HoPhD,
	author		= {Ho, C.-M. R.},
	title			= {Validation Tools for Complex Digital Designs},
	year			= {1996},
}

@BOOK{PowerPC,
  AUTHOR =       {B. Frey},
  TITLE =        {PowerPC Architecture Book},
  YEAR =         {2005},
  publisher = {IBM},
}

@BOOK{IA32,
  TITLE =        {IA-32 Intel Architecture Software Developer's Manual},
  PUBLISHER =    {Intel},
  YEAR =         {2006},
}

@BOOK{PentiumPro,
  TITLE =        {Pentium Pro Family Developer’s Manual Volume 3: Operating System Writer’s Guide},
  PUBLISHER =    {Intel},
  YEAR =         {1996},
}


@MISC{QFBV,
  note =        {http://goedel.cs.uiowa.edu/smtlib/logics/QF\_BV.smt},
}

@ARTICLE{IntelValidation,
  AUTHOR =       {B. Bentley and R. Gray},
  TITLE =        {Validating the Intel Pentium 4 Processor},
  JOURNAL =      {Intel Technology Journal},
  YEAR =         {2001},
}

%%% уточнить название!
@ARTICLE{KamkinPopular,
  AUTHOR =       {Камкин, А. С.},
  TITLE =        {Функциональная верификация микропроцессоров: борьба с ошибками и управление качеством},
  JOURNAL =      {Электроника: Наука, Технология, Бизнес},
  YEAR =         {2010},
  number =       {3},
}

@BOOK{EDAbook,
  AUTHOR =       {Wang, L.-T. and  Chang, Y.-W. and Cheng, K.-T.},
  TITLE =        {Electronic Design Automation: Synthesis, Verification, and Test},
  PUBLISHER =    {Morgan Kaufmann},
  YEAR =         {2009},
}

@PHDTHESIS{KamkinThesis,
  AUTHOR =       {Камкин, А. С.},
  TITLE =        {Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций},
  SCHOOL =       {Институт системного программирования РАН},
  YEAR =         {2009},
}

@BOOK{IvanPreprint,
  AUTHOR =       {Иванников, В. П. and Камкин, А. С. and Кулямин, В. В. and Петренко, А. К.},
  TITLE =        {Применение технологии UniTESK для функционального тестирования моделей аппаратного обеспечения},
  PUBLISHER =    {Препринт Института системного программирования РАН},
  YEAR =         {2005},
  number =       {8},
  address =      {M.},
  pages =        {26},
}

